﻿namespace Coq.MonoDevelop

open System
open System.IO
open System.Diagnostics
open System.Text
open System.Text.RegularExpressions
open System.Collections.Generic

open MonoDevelop.Ide
open MonoDevelop.Core

type Message = 
    | Error of String * Option<(int*int)>
    | Output of String 
    | Proof of String

type CoqSession() =
    let server = "MonoDevelop" + Guid.NewGuid().ToString("n")
    //let path = Path.Combine(Environment.GetFolderPath(Environment.SpecialFolder.ProgramFiles),"Coq\\bin\\");
    let file = new FileInfo(System.Reflection.Assembly.GetExecutingAssembly().Location)
    let path = Path.Combine(file.DirectoryName,"Coq\\bin\\");
    let exec = "CoqTop.exe" 
    let fullpath = Path.Combine(path, exec);

    let mutable waitingForResponse = false

    let coqProcess = 
        let startInfo = 
            new ProcessStartInfo (FileName = fullpath, UseShellExecute = false, Arguments = "", RedirectStandardError = true, CreateNoWindow = true, RedirectStandardOutput = true, RedirectStandardInput = true) 
        try 
            Debug.WriteLine("Starting Coq Process");
            Process.Start(startInfo)
        with e -> 
            Debug.WriteLine("Starting Coq Process raised exeption");
            reraise()

    let textReceived = new Event<_>()  
    let promptReady = new Event<_>()  

    do 
        Event.merge coqProcess.OutputDataReceived coqProcess.ErrorDataReceived
            |> Event.filter (fun de -> de.Data <> null)
            |> Event.add (fun de ->
                Debug.WriteLine("recieved") 
                if (de.Data.Trim().StartsWith("coq <")) then
                    Debug.WriteLine("ready")
                    DispatchService.GuiDispatch(fun () -> promptReady.Trigger())
                elif de.Data.Trim() <> "" then
                    let str = (if waitingForResponse then waitingForResponse <- false; "\n" else "") + de.Data + "\n"
                    Debug.WriteLine("sent")
                    DispatchService.GuiDispatch(fun () -> textReceived.Trigger(str)) )
        coqProcess.EnableRaisingEvents <- true

    member x.Interrupt() =
        Debug.WriteLine("Break!")
        //client.Interrupt()

    member x.Restart() = 
            coqProcess.Kill()
            coqProcess.Start()
    
    member x.StartReceiving() = 
        coqProcess.BeginOutputReadLine()  
        coqProcess.BeginErrorReadLine()
    
    member x.TextReceived = textReceived.Publish
    member x.PromptReady = promptReady.Publish
  
    member x.Kill() = 
        coqProcess.Kill()
        
        
    member x.SendCommand(str:string) = 
        waitingForResponse <- true
        Debug.Write("Sending------------------") 
        let sendString = str + " Locate aCPELXO23."
        coqProcess.StandardInput.WriteLine(sendString) 
        Debug.WriteLine(sendString)
        let rs = new StringBuilder();
        let stream = coqProcess.StandardOutput

        Debug.WriteLine("still alive")

        //read reaction from std out. We discover the end thanks to errorline with "CPELXO23"
        let mutable continueLooping = true;
        let mutable isError = false;
        let mutable isProof = false;
        while (continueLooping) do
            let l = stream.ReadLine();
            Debug.WriteLine(l)
            if (l.Contains("aCPELXO23")) then
                continueLooping <- false
            else
                if (l.StartsWith("Error")=true || l.StartsWith("Syntax error")=true) then
                    isError <- true
                if (l.Contains("subgoal") = true) then
                    isProof <- true
                rs.AppendLine(l) |> ignore
        Debug.WriteLine ("Finished") 

        //return
        if (isError) then
            let pattern = ", characters ([0-9]+)-([0-9]+):" 
            let returnstring = rs.ToString()

            let m = Regex.Match(returnstring, pattern);
            
            //To get location from regexp
            if (m.Groups.Count>1) then 
                Error(returnstring,Some(Int32.Parse(m.Groups.Item(1).Value), Int32.Parse(m.Groups.Item(2).Value)))
            else
                Error(returnstring,None)
        else if (isProof) then
            Proof(rs.ToString())
        else
            Output(rs.ToString())
        

    member x.Exited = coqProcess.Exited